home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / simplify_2.06.2 < prev    next >
Text File  |  1992-04-03  |  14KB  |  432 lines
  1. %%% SIMPLIFY
  2. %%% version 2.04.6 (based on simplify 18.4)
  3. %%%   added fixed_priority
  4. %%% version 2.05.3
  5. %%%   added support for Quintus Prolog
  6. %%% version 2.06.0
  7. %%%   added bug fixes from Shie-Jue
  8. %%% version 2.06.2
  9. %%%   fixed Quintus Prolog existence error in duplicate deletion
  10. %%%
  11. %%% This module performs four tasks:
  12. %%%    tautology deletion
  13. %%%    unit simplification
  14. %%%    ground unit clause generation
  15. %%%    duplicate deletion
  16.  
  17. %%% Unit subsumption never fails.
  18. %%% Unit simplification succeeds if a simplified clause is an empty clause.
  19. %%% Tautology deletion never fails.
  20. %%% Duplicate deletion never fails.
  21.  
  22. %%% We take advantage of the fast unification in prolog. Put unit clauses
  23. %%%     separately.
  24. %%% In order to check subsumption for unit clauses, we number the original
  25. %%%    unit clauses and generated unit clauses, so that a unit clause 
  26. %%%    won't be sumbsumed by itself.
  27.      fol_simplify :-
  28.     check_tautology_deletion.
  29.      fol_simplify :-
  30.     not(not(check_unit_simp)), !.
  31.      fol_simplify :-
  32.     gug.
  33.      fol_simplify :-
  34.     check_duplicate_deletion.
  35.  
  36. %%% Tautology deletions.
  37.      check_tautology_deletion :-
  38.     tautology_deletion,
  39.     cputime(TT1),
  40.     const_list(Clist),
  41.     tautology_deletion(Clist),
  42.     cputime(TT2),
  43.     TT3 is TT2 -TT1,
  44.     write_line(5,'Tautology deletion(s): ',TT3), 
  45.     !, fail.
  46.  
  47. %%% Unit simplification/subsumption.
  48.      check_unit_simp :-
  49.     unit_resolution,
  50.     cputime(TT1),
  51.     abolish(new_unit_clause,0),
  52.     unit_simp_subs(Res),
  53.     cputime(TT2),
  54.     TT3 is TT2 -TT1,
  55.     write_line(5,'Unit simplification(s): ',TT3), 
  56.     !, Res == suc.
  57.  
  58.  
  59. %%% Ground unit generation. If a non-unit clause C having only one ground
  60. %%%    literal L, the non-ground literals can be unified with unit clauses,
  61. %%%    then C can be replaced by L.
  62.      gug :-
  63.     cputime(TT1),
  64.     gug_1,
  65.     cputime(TT2),
  66.     TT3 is TT2 - TT1,
  67.     write_line(5,'Ground unit generation(s): ',TT3),
  68.     !, fail.
  69.  
  70. %%% Duplicate deletions.
  71.      check_duplicate_deletion :-
  72.     unit_resolution,
  73.     cputime(TT1),
  74.     const_list(Clist),
  75.     bagof1(Ref1,nonunitcl(Ref1),Refs1),
  76.     duplicate_deletion(Refs1,Clist),
  77.     physically_erase(sent_C),
  78.     cputime(TT2),
  79.     TT3 is TT2 -TT1,
  80.     write_line(5,'Duplicate deletion(s): ',TT3), 
  81.     !, fail.
  82.  
  83. %%% Find reference for non-unit clauses.
  84.      nonunitcl(X) :-
  85.     clause(sent_C(cl(_,_,by([_,_|_],_,_,_,_),_,_,_,_,_,_)),true,Ref1),
  86.     X = Ref1.
  87.  
  88. %%% Perform tautology deletion.
  89.      tautology_deletion(Clist) :-
  90.     clause(sent_C(cl(_,_,by([L1,L2|Ls],V11,V11,Clist,_),_,_,_,_,_,_)),
  91.         true,Ref1),
  92.     tautology_clause([L1,L2|Ls]),
  93.     erase(Ref1),
  94.     fail.
  95.      tautology_deletion(_).
  96.  
  97. %%% Perform unit simplification/subsumption.
  98.      unit_simp_subs(Res) :-
  99.     sent_C(cl(_,_,by([_],_,_,_,_),_,_,_,_,_,_)),
  100.     init_num,
  101.     move_unit_clauses,
  102.     unit_simp_subs_1(Res), !.
  103.      unit_simp_subs(nsuc).
  104.  
  105. %%% Move unit clauses to ou clauses.
  106. %%% Number the unit clauses.
  107.      move_unit_clauses :-
  108.     retract(sent_C(cl(CSize1,CN1,by([L1],V11,V12,V1,W1),
  109.         CI1,CS1,CR1,CT1,CF1,CP1))),
  110.     next_num(N),
  111.     assertz(ou(cl(CSize1,CN1,by([L1],V11,V12,V1,W1),
  112.         CI1,CS1,CR1,CT1,CF1,CP1),N)),
  113.     fail.
  114.      move_unit_clauses.
  115.     
  116. %%% In order to effiently matched unit clauses, we keep them in a separate
  117. %%%     database, since we don't need to care about the simplification of
  118. %%%    unit clause ( We stop whenever a unit clause is simplified by 
  119. %%%    another unit clause ). 
  120. %%% We keep a special data structure for nonunit clauses. We don't update
  121. %%%    the clauses directly in the database, but update the special
  122. %%%    data structure instead.
  123.      unit_simp_subs_1(Res) :-
  124.     const_list(Clist),
  125.     bagof1(X,transtrps(X),Trps),
  126.     unit_simp_subs_2(Clist,Trps,Res), !.
  127.  
  128. %%% Obtain a special data structure for non-unit clauses.
  129.      transtrps(X) :-
  130.     clause(sent_C(cl(_,_,by(Cn,_,_,_,_),_,CS,_,_,_,_)),true,FF),
  131.     corresp_ordinals_list(Cn,Flags),
  132.     X = us(CS,FF,Flags,0).
  133.  
  134. %%% unit_simp_subs_3 succeeds if an empty clause is found.
  135.      unit_simp_subs_2(Clist,Trps1,Tag) :-
  136.     unit_simp_subs_3(Clist,Trps1,Trps2,Tag),
  137.     unit_simp_subs_2_1(Tag,Clist,Trps2).
  138.  
  139. %%% If unsatisfiable, then done.
  140.      unit_simp_subs_2_1(Tag,_,Trps2) :- 
  141.     Tag == suc, 
  142.     unit_simp_subs_hk(Trps2),
  143.     !.
  144. %%% If new unit clauses are generated in the last iteration, start 
  145. %%%    another round of iteration.
  146.      unit_simp_subs_2_1(Tag,Clist,Trps2) :-
  147.     retract(new_unit_clause),
  148.     unit_simp_subs_2(Clist,Trps2,Tag), !.
  149. %%% If no new unit clauses are generated in the last iteration, stop.
  150.      unit_simp_subs_2_1(nsec,_,Trps2) :-
  151.     unit_simp_subs_hk(Trps2).
  152.  
  153. %%% Simplify/subsumes unit clauses first.
  154.      unit_simp_subs_3(Clist,Trps2,Trps2,Tag) :-
  155.     unit_clause_simp_subs(Clist,Tag), !.
  156. %%% Simplify/subsumes nonunit clauses.
  157.      unit_simp_subs_3(Clist,Trps1,Trps2,Tag) :-
  158.     non_unit_clause_simp_subs(Clist,Trps1,Trps2,Tag), !.
  159.  
  160. %%% Simplification/subsumption for unit clauses.
  161.      unit_clause_simp_subs(Clist,Tag) :-
  162.     pick_unit_clause_simp_subs(Clist,Ln1,N1,Ref1),
  163.     negate(Ln1,NLn1),
  164.     unit_clause_simp_subs_1(Ln1,NLn1,N1,Ref1,Tag), !.
  165.  
  166. %%% Pick a unit clause to be sumbumed or simplified.
  167.      pick_unit_clause_simp_subs(Clist,Ln1,N1,Ref1) :-
  168.     clause(ou(cl(_,_,by([Ln1],V11,V11,Clist,_),_,_,_,_,_,_),N1),
  169.         true,Ref1).
  170.      pick_unit_clause_simp_subs(Clist,Ln1,N1,Ref1) :-
  171.     clause(du(cl([Ln1],Clist,_,_,_,_,_,_),N1),true,Ref1).
  172.  
  173. %%% Find if a unit clause subsumes the underlying literal.
  174.      unit_clause_simp_subs_1(_,NLn1,_,_,suc) :-
  175.     unit_clause_unit_matched(NLn1,_), !.
  176.      unit_clause_simp_subs_1(Ln1,_,N1,Ref1,_) :-
  177.     unit_clause_unit_matched(Ln1,N1),
  178.     erase(Ref1), !, fail.
  179.  
  180. %%% Find if a unit clause simplifies the underlying unit clause.
  181. %%% First check the unit clauses ou.
  182.      unit_clause_unit_matched(Ln1,N1) :-
  183.     ou(cl(_,_,by([Ln1],V11,V11,_,_),_,_,_,_,_,_),N2),
  184.     N1 \== N2, !.
  185. %%% Then check the unit clauses du.
  186.      unit_clause_unit_matched(Ln1,N1) :-
  187.     du(cl([Ln1],_,_,_,_,_,_,_),N2), N1 \== N2, !.
  188.  
  189. %%% Find if a unit clause simplifies the underlying literal.
  190. %%% First check the unit clauses ou.
  191.      non_unit_clause_unit_match(Ln1,CS2) :-
  192.     ou(cl(_,_,by([Ln1],V11,V11,_,_),_,CS2,_,_,_,_),_), !.
  193. %%% Then check the unit clauses du.
  194.      non_unit_clause_unit_match(Ln1,CS2) :-
  195.     du(cl([Ln1],_,_,_,CS2,_,_,_),_), !.
  196.  
  197. %%% Simplification/subsumption for nonunit clauses.
  198. %%% Do one non-unit clause at a time.
  199.      non_unit_clause_simp_subs(Clist,[Trp1|Trps1],Trps2,Tag) :-
  200.     Trp1 = us(CS1,Ref1,Flags1,_),
  201.     clause(sent_C(cl(_,_,by(Cn1,V11,V11,Clist,_),_,_,_,_,_,_)),
  202.         true,Ref1),
  203.     clause_remain_1(Flags1,1,Cn1,CnM),
  204.     unit_reso_clause(Trp1,CnM,CS1,Ref1,Flags1,Trps2,Trps3,Tag),
  205.     !,
  206.     non_unit_clause_simp_subs_1(Tag,Clist,Trps1,Trps3).
  207.      non_unit_clause_simp_subs(_,[],[],_).
  208.  
  209.      non_unit_clause_simp_subs_1(Tag,_,Trps1,Trps1) :- Tag == suc, !.
  210.      non_unit_clause_simp_subs_1(Tag,Clist,Trps1,Trps3) :-
  211.     non_unit_clause_simp_subs(Clist,Trps1,Trps3,Tag).
  212.  
  213. %%% If the underlying clause can be neither subsumped nor simplified,
  214. %%%     unit_reso_literals would fail.
  215.      unit_reso_clause(Trp1,Cn1,CS1,Ref1,Flags1,Trps2,Trps3,Tag) :-
  216.     unit_reso_literals(CS1,Flags1,Cn1,CS3,Flags3,Cn3,Res,_), !,
  217.     update_trps(Cn3,Res,Flags3,CS3,Ref1,Trps2,Trps3,Tag).
  218.      unit_reso_clause(Trp1,_,_,_,_,[Trp1|Trps2],Trps2,_).
  219.  
  220.      unit_reso_literals(_,_,[Ln1|_],_,_,d,n,_) :-
  221.     non_unit_clause_unit_match(Ln1,_), !.
  222.      unit_reso_literals(CS1,[_|Flags1],[Ln1|Lns1],CS3,Flags3,Cn3,Var1,s) :-
  223.     negate(Ln1,NLn1),
  224.     non_unit_clause_unit_match(NLn1,CS2),
  225.     binary_max(CS1,CS2,CSM), !,
  226.     unit_reso_literals(CSM,Flags1,Lns1,CS3,Flags3,Cn3,Var1,s).
  227.      unit_reso_literals(CS1,[Flag1|Flags1],[Ln1|Lns1],CS3,[Flag1|Flags3],
  228.         [Ln1|Cn3],Var1,Var2) :-
  229.          unit_reso_literals(CS1,Flags1,Lns1,CS3,Flags3,Cn3,Var1,Var2).
  230.      unit_reso_literals(_,[],_,_,_,_,_,n) :- !, fail.
  231.      unit_reso_literals(CS3,[],_,CS3,[],[],_,_).
  232.  
  233. %%% Update the non-unit clause list.
  234.      update_trps([],_,Flags3,CS3,Ref1,[us(CS3,Ref1,Flags3,1)|Trps3],
  235.         Trps3,suc) :- !.
  236.      update_trps(Cn3,s,Flags3,CS3,Ref1,Trps2,Trps3,_) :-
  237.     update_trps_1(Flags3,CS3,Ref1,Trps2,Trps3), !.
  238.      update_trps(_,n,_,_,Ref1,Trps2,Trps2,_) :- erase(Ref1).
  239.  
  240. %%% If the underlying clause is simplified to unit clause, then 
  241. %%%    assert it into database as du clause and number it.
  242. %%% Otherwise, modified one entry in the special list.
  243.      update_trps_1([Flag2],CS2,Ref1,Trps2,Trps2) :-
  244.     clause(sent_C(cl(_,_,by(Cn1,V11,V11,_,W1),CI1,CS1,CR1,CT1,CF1,_)),
  245.         true,Ref1),
  246.     erase(Ref1),
  247.     clause_remain_3([Flag2],1,Cn1,W1,CF1,Cn3,W3,CF3),
  248.     vars_W1_V1(W3,V3),
  249.     update_trps_CS(CS2,CS1,Cn3,CS3),
  250.     assert_once(new_unit_clause),
  251.     next_num(N1),
  252.     assertz(du(cl(Cn3,V3,W3,CI1,CS3,CR1,CT1,CF3),N1)), !.
  253.      update_trps_1(Flags3,CS3,Ref1,[us(CS3,Ref1,Flags3,1)|Trps3],Trps3).
  254.  
  255. %%% Housekeeping clauses.
  256. %%% Deals with unit clauses.
  257.      unit_simp_subs_hk(_) :-
  258.     unit_simp_subs_hk_1, !.
  259. %%% Modified non-unit clauses.
  260.      unit_simp_subs_hk(Trps1) :-
  261.     unit_simp_subs_hk_2(Trps1), !.
  262.     
  263.  
  264. %%% Move du clauses to sent_C clauses.
  265.      unit_simp_subs_hk_1 :-
  266.     retract(du(DU1,_)),
  267.     unit_simp_subs_hk_1_d(DU1),
  268.     fail.
  269. %%% Move ou clauses to sent_C clauses.
  270.      unit_simp_subs_hk_1 :-
  271.     retract(ou(OU1,_)),
  272.     unit_simp_subs_hk_1_o(OU1),
  273.     fail.
  274.  
  275. %%% Modified non-unit clauses.
  276.      unit_simp_subs_hk_1_d(cl(Cn1,V1,W1,CI1,CS1,CR1,CT1,CF1)) :- 
  277.     linearize_term(Cn1,Cn3,V31,V32),
  278.     clause_size(Cn1,CSize1),
  279.     calculate_priority_clause(Cn1,CS1,CR1,CP1),
  280.     compute_V_lits(W1,0,CV1),
  281.     asserta(sent_C(cl(CSize1,CV1,by(Cn3,V31,V32,V1,W1),
  282.         CI1,CS1,CR1,CT1,CF1,CP1))), !.
  283.      unit_simp_subs_hk_1_o(OU1) :-
  284.     asserta(sent_C(OU1)), !.
  285.  
  286.      unit_simp_subs_hk_2([us(_,_,_,0)|Trps1]) :-
  287.     !, unit_simp_subs_hk_2(Trps1).
  288.      unit_simp_subs_hk_2([us(CSM,Ref1,Flags1,1)|Trps1]) :-
  289.     clause(sent_C(cl(_,_,by(Cn1,V11,V11,_,W1),
  290.         CI1,CS1,CR1,CT1,CF1,pr(_,_,_,PR1,_))),true,Ref1),
  291.     erase(Ref1),
  292.     clause_remain_3(Flags1,1,Cn1,W1,CF1,CnM,W3,CF3),
  293.     linearize_term(CnM,Cn3,V31,V32),
  294.     vars_W1_V1(W3,V3),
  295.     compute_V_lits(W3,0,CV3),
  296.     clause_size(CnM,CSize1),
  297.     update_trps_CS(CSM,CS1,CnM,CS3),
  298.     priority_NewPSPDPL(CnM,CS3,PS3,PD3,PL3),
  299.     maximum(PS3,PD3,Temp1),
  300.     maximum(Temp1,PL3,Temp2),
  301.     maximum(Temp2,PR1,PX3),
  302.     assertz(sent_C(cl(CSize1,CV3,by(Cn3,V31,V32,V3,W3),CI1,
  303.         CS3,CR1,CT1,CF3,pr(PS3,PD3,PL3,PR1,PX3)))),
  304.     !, unit_simp_subs_hk_2(Trps1).
  305.      unit_simp_subs_hk_2([]).
  306.     
  307.      update_trps_CS(CS1,CS2,Cn3,CS3) :-
  308.     pn_clause(Cn3,F),
  309.     update_trps_CS_1(F,CS1,CS2,CS3).
  310.      update_trps_CS(sp(S11,_,_),sp(S21,S22,S23),_,sp(S31,S22,S23)) :-
  311.     binary_max(S11,S21,S31).
  312.  
  313.      update_trps_CS_1(p,CS1,CS2,CS3) :-
  314.     update_trps_CS_1_p(CS1,CS2,CS3), !.
  315.      update_trps_CS_1(n,CS1,CS2,CS3) :-
  316.     update_trps_CS_1_n(CS1,CS2,CS3), !.
  317.  
  318.      update_trps_CS_1_p(sp(S11,_,S13),sp(S21,S22,S23),sp(S31,S22,S33)) :-
  319.     binary_max(S11,S21,S31),
  320.     binary_max(S13,S23,S33).
  321.  
  322.      update_trps_CS_1_n(sp(S11,S12,_),sp(S21,S22,S23),sp(S31,S32,S23)) :-
  323.     binary_max(S11,S21,S31),
  324.     binary_max(S12,S22,S32).
  325.  
  326.      priority_NewPSPDPL(_,_,0,0,0) :-
  327.     not(fixed_priority),
  328.     not(slidepriority),
  329.     !.
  330.      priority_NewPSPDPL(Cn1,CS1,PS,PD,PL) :-
  331.     depth_coef(DCoef),
  332.     size_coef(SCoef),
  333.     literal_coef(LCoef),
  334.     priority_PS(SCoef,Cn1,PS),
  335.     priority_PD(DCoef,Cn1,PD),
  336.     priority_PL(LCoef,Cn1,CS1,PL), !.
  337.  
  338. %%% Perform ground unit clause generation.
  339.      gug_1 :-
  340.     clause(sent_C(cl(_,CV1,by(Cn1,V11,V11,_,Ws1),CI1,
  341.         CS1,CR1,CT1,FB1,_)),true,Ref1),
  342.     CV1 \== 0,
  343.     length(Cn1,CL1),
  344.     CL1 is CV1 + 1,
  345.          gug_1_1(FB1,Cn1,Ws1,CS1,CR1,CI1,CT1,Ref1),
  346.     fail.
  347.      gug_1.
  348.  
  349.      gug_1_1(FB1,Cn1,Ws1,CS1,CR1,CI1,CT1,Ref1) :-
  350.     sep_gr_lit_3(Ws1,FB1,Cn1,W21,Ws2,F2,_,L2,Ls2),
  351.     negate_clause(Ls2,NLs2),
  352.     clause_part2(CS1,CR1,CSM,CRM),
  353.     !, gug_1_1_1(NLs2,Ws2,CSM,CRM,CSM2,CRM2),
  354.     calculate_S([L2],_,CSM,CS2),
  355.     adjust_userdist(CRM2,CR1,CR2),
  356.     clause_size([L2],CSize2),
  357.     calculate_priority_clause([L2],CS2,CR2,CP2),
  358.     erase(Ref1),
  359.     assertz(sent_C(cl(CSize2,0,by([L2],[],[],V2,[W21]),
  360.         CI1,CS2,CR2,CT1,[F2],CP2))), !.
  361.  
  362. %%% Unify with unit clauses.
  363.      gug_1_1_1(Cn1,Ws1,CS1,CR1,CS2,CR2) :-
  364.     sep_gr_lit_2(Ws1,Cn1,W21,Ws2,L2,Ls2),
  365.     !, gug_unify_unit(L2,CS1,CR1,CSM,CRM),
  366.     !, gug_1_1_1(Ls2,Ws2,CSM,CRM,CS2,CR2).
  367.      gug_1_1_1([L1|Ls1],[_|Ws1],CS1,CR1,CS2,CR2) :-
  368.     gug_unify_unit(L1,CS1,CR1,CSM,CRM),
  369.     w1_w2(Ws1,Ws2),
  370.     gug_1_1_1(Ls1,Ws2,CSM,CRM,CS2,CR2).
  371.      gug_1_1_1([],_,CS2,CR2,CS2,CR2).
  372.  
  373. %%% Unify with one unit clause.
  374.      gug_unify_unit(L1,CS1,CR1,CS2,CR2) :-
  375.     sent_C(cl(_,_,by([L1],V11,V12,_,_),_,CSU,CRU,_,_,_)),
  376.     unify_lists(V11,V12),
  377.     onematch_SR(L1,CS1,CR1,CSU,CRU,CS2,CR2).
  378.  
  379. %%% Perform duplicate deletion.
  380. %%% Check one clause at a time.
  381.      duplicate_deletion([Ref1|Refs1],Clist) :-
  382.     clause(sent_C(cl(CSize1,CN1,by(Cn1,V11,V11,Clist,_),CI1,
  383.         CS1,CR1,CT1,F1,pr(_,_,PL1,_,PX1))),true,Ref1),
  384.     not(logically_erased(sent_C,Ref1)),
  385.     duplicate_deletion_1(Clist,CSize1,CN1,Cn1,CI1,CS1,CR1,CT1,F1,
  386.         PL1,PX1,Ref1,Refs1,RefsR),
  387.     !,
  388.     duplicate_deletion(RefsR,Clist).
  389.      duplicate_deletion([_|Refs1],Clist) :-
  390.     !, duplicate_deletion(Refs1,Clist).
  391.      duplicate_deletion([],_).
  392.     
  393. %%% Find duplicates.
  394.      duplicate_deletion_1(Clist,CSize1,CN1,Cn1,CI1,CS1,CR1,CT1,F1,PL1,PX1,
  395.         Ref1,Refs1,RefsR) :-
  396.     duplicate_deletion_2(Refs1,Clist,CSize1,CN1,Cn1,CI1,CS1,CR1,CT1,F1,
  397.         PL1,PX1,CI3,CS3,CR3,CT3,F3,PL3,PX3,Up,RefsR),
  398.     duplicate_deletion_3(Up,CI3,CS3,CR3,CT3,F3,PL3,PX3,Ref1).
  399.  
  400.      duplicate_deletion_3(n,_,_,_,_,_,_,_,_) :- !.
  401.      duplicate_deletion_3(_,CI3,CS3,CR3,CT3,F3,PL3,PX3,Ref1) :-
  402.     clause(sent_C(cl(CSize1,CN1,BY_1,_,_,_,_,_,pr(PS1,PD1,_,_,_))),
  403.         true,Ref1),        
  404.     logically_erase(sent_C,Ref1),
  405.     priority_NewPR(CR3,PR3),
  406.     assertz(sent_C(cl(CSize1,CN1,BY_1,CI3,CS3,CR3,CT3,F3,
  407.         pr(PS1,PD1,PL3,PR3,PX3)))), !.
  408.  
  409. %%% Find all duplicates, and modify the information if necessary.
  410.      duplicate_deletion_2([Ref2|Refs2],Clist,CSize1,CN1,Cn1,CI1,CS1,CR1,
  411.         CT1,F1,PL1,PX1,CIO,CSO,CRO,CTO,FO,PLO,PXO,Up,RefsR) :-
  412.     clause(sent_C(cl(CSize1,CN1,by(Cn1,V22,V22,Clist,_),
  413.         CI2,CS2,CR2,CT2,F2,pr(_,_,PL2,_,PX2))),true,Ref2),
  414.     not(logically_erased(sent_C,Ref2)),
  415.     min_ind(PL1,PL2,PL3,Up),
  416.     min_ind(PX1,PX2,PX3,Up),
  417.     min_Flags_ind(F1,F2,F3,Up),
  418.     max_CS_ind(CS1,CS2,CS3,Up),
  419.     min_CR_ind(CR1,CR2,CR3,Up),
  420.     binary_max_ind(CI1,CI2,CI3,Up),
  421.     binary_max_ind(CT1,CT2,CT3,Up),
  422.     logically_erase(sent_C,Ref2),
  423.     !,
  424.     duplicate_deletion_2(Refs2,Clist,CSize1,CN1,Cn1,CI3,CS3,CR3,CT3,F3,
  425.         PL3,PX3,CIO,CSO,CRO,CTO,FO,PLO,PXO,Up,RefsR).
  426.      duplicate_deletion_2([Ref2|Refs2],Clist,CSize1,CN1,Cn1,CI1,CS1,CR1,
  427.         CT1,F1,PL1,PX1,CIO,CSO,CRO,CTO,FO,PLO,PXO,Up,[Ref2|RefsR]) :-
  428.     duplicate_deletion_2(Refs2,Clist,CSize1,CN1,Cn1,CI1,CS1,CR1,
  429.         CT1,F1,PL1,PX1,CIO,CSO,CRO,CTO,FO,PLO,PXO,Up,RefsR).
  430.      duplicate_deletion_2([],_,_,_,_,CIO,CSO,CRO,CTO,FO,PLO,PXO,
  431.         CIO,CSO,CRO,CTO,FO,PLO,PXO,_,[]).
  432.